Why lists?

Originally, I wanted lists in TEX for a paper I was writing which contained a lot of facts.

<#2033#>Fact <#2033#>   <#2035#>by 1 Number-Fac-cows<#755#><#755#>Label-<#756#><#756#> Cows have four legs.<#2035#>

<#2037#>Fact <#2037#>   <#2039#>by 1 Number-Fac-people<#757#><#757#>Label-<#758#><#758#> People have two legs.<#2039#>

<#2041#>Fact <#2041#>   <#2043#>by 1 Number-Fac-yawn<#759#><#759#>Label-<#760#><#760#> Lots of facts in a row can be dull.<#2043#>

These are generated with commands like 
verbatim61#
I can then refer to these facts by saying 
verbatim62#
to get :<#768#><#770#>Foldr@<#774#>@<#774#><#647#><<#775#><<#781#>Insert@<#786#>@<#786#><#787#><#787#><#781#><#653#><<#782#><#782#><#783#><#783#>653>><#775#><#651#><<#776#><<#776#><#777#><#777#>651>>647>><#770#><#645#><<#771#><<#778#>Insert@<#784#>@<#784#><#785#><#785#><#778#><#667#><<#779#><#779#><#780#><#780#>667>><#771#><#665#><<#772#><<#772#><#773#><#773#>665>>645>><#768#><#769#><#769#>!:}:<#792#><#794#>Foldr@<#796#>@<#796#><#697#>6<#800#><#802#><<#802#><#800#><#801#><<#801#>7>><#794#><#695#>6<#803#><#805#><<#805#><#803#><#804#><<#804#>5>><#792#><#793#><#793#>!:}Number-:;SPMlt;Foldr@<#789#>7<#808#>Label-<<#808#><#809#><<#809#>9>><#790#><#790#> <#763#><#763#>!:}[Fac-yawn,Fac-cows,Fac-people]. And as if by magic, the facts come out sorted, rather than in the jumbled order I typed them. This is very useful, as I can reorganize my document to my heart's content, and not have to worry about getting my facts straight.

Originally I tried programming this sorting routine in TEX's list macros, from Appendix~D of , but I soon ran into trouble. The problem is that all the Appendix~D macros work by assigning values to macros. For example: 

verbatim63#
expands out to 
verbatim64#
which assigns the macro 1 the contents of 2 followed by the contents of 3. Programming sorting routines (which are usually recursive) in terms of these lists became rather painful, as I was constantly having to watch out for local variables, worrying about what happened if a local variable had the same name as a global one, and generally having a hard time.

Then I had one of those ``flash of light'' experiences --- ``You can do lambda-calculus in TEX,'' I thought, and since you can do lists directly in lambda calculus, you should be able to do lists straightforwardly in TEX. And so you can. Well, fairly straightforwardly anyway.

So I went and did a bit of mathematics, and derived the TEX macros you see here. They were formally verified, and worked first time (modulo typing errors, of which there were two).